#ifndef TERVEC_H
#define TERVEC_H

#include <vector>
#include <cstdint>
#include <string>

typedef uint8_t Word;

class TerVec {
private:
    std::vector<Word> ref;  // Each bit represents a variable
    std::vector<Word> pol;  // Each bit represents polarity
    size_t maxVar;             // Highest variable index used

    // Helper function to set/get bits
    static void setBit(Word& word, int pos, bool value);
    static bool getBit(Word word, int pos);

public:
    // Construct from DIMACS format (e.g., {3, -4, 5})
    explicit TerVec(const std::vector<int>& literals);
    size_t getMaxVar() const { return maxVar; }
    
    // Access the vectors
    const std::vector<Word>& getRef() const { return ref; }
    const std::vector<Word>& getPol() const { return pol; }
    
    // Check if variable is present and get its polarity
    bool hasVar(size_t var) const;
    bool getPolarity(size_t var) const;  // true if negative
    
    // Convert back to DIMACS format for debugging
    std::string toDIMACS() const;
    
    // Get number of literals in clause
    size_t numLiterals() const;
};

#endif 